$\forall$$T$:Type, $P$:($T$$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$x$:$T$. Dec($P$($x$)))
\\[0ex]$\Rightarrow$ ($\forall$$L$:($T$ List). $\exists$$X$,$Y$:$T$ List. ($L$ = ($X$ @ $Y$) \& ($\forall$$x$$\in$$X$. $\neg$$P$($x$)) \& (($\parallel$$Y$$\parallel$ $\geq$ 1 ) $\Rightarrow$ $P$(hd($Y$)))))